i:Id, M:{M:MsgA| Feasible(M) }. @i: M  System 

latex

Definitions	x:A. B(x), t  T, System, @i: A, if b t else f fi, P  Q, true, Prop, false, , Unit, P  Q, P & Q,
Lemmas	ifthenelse wf, eq id wf, ma-empty wf, Id wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert-eq-id, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, ma-feasible wf, msga wf, ma-empty-feasible